#include "tervec.h"
#include <algorithm>

void TerVec::setBit(uint8_t& byte, int pos, bool value) {
    const int mask = 1 << (pos % 8);
    byte = value ? (byte | mask) : (byte & ~mask);
}

bool TerVec::getBit(uint8_t byte, int pos) {
    return (byte >> (pos % 8)) & 1;
}

TerVec::TerVec(const std::vector<int>& literals) {
    // Find highest variable index
    maxVar = 0;
    for (int lit : literals) {
        maxVar = std::max(maxVar, static_cast<size_t>(std::abs(lit)));
    }
    
    size_t vecSize = (maxVar + 7) / 8;  // ceiling division
    ref.resize(vecSize, 0);
    pol.resize(vecSize, 0);
    
    // Set reference and polarity bits
    for (int lit : literals) {
        size_t var = std::abs(lit) - 1;  // Convert to 0-based index
        size_t byteDex = var / 8;
        size_t bitDex = var % 8;
        
        setBit(ref[byteDex], bitDex, 1);  // Mark variable as present
        setBit(pol[byteDex], bitDex, lit < 0);  // Set polarity
    }
}

bool TerVec::hasVar(size_t var) const {
    if (var >= maxVar) return false;
    size_t byteDex = var / 8;
    size_t bitDex = var % 8;
    return getBit(ref[byteDex], bitDex);
}

bool TerVec::getPolarity(size_t var) const {
    if (var >= maxVar) return false;
    size_t byteDex = var / 8;
    size_t bitDex = var % 8;
    return getBit(pol[byteDex], bitDex);
}

std::string TerVec::toDIMACS() const {
    std::string result;
    for (size_t var = 0; var < maxVar; var++) {
        if (hasVar(var)) {
            if (!result.empty()) result += " ";
            int lit = var + 1;  // Convert to 1-based index
            result += getPolarity(var) ? std::to_string(-lit) : std::to_string(lit);
        }
    }
    return result + " 0";
}

size_t TerVec::numLiterals() const {
    size_t count = 0;
    for (size_t var = 0; var < maxVar; var++) {
        if (hasVar(var)) count++;
    }
    return count;
} 